ds:x:Id fp Type, da:k:Knd fp Type, a:ecl(ds;da), v:ecl-trans-tuple{i:l}(ds;da),
L:event-info(ds;da) List.
(L:event-info(ds;da) List.
(ecl-trans-normal(v) & (n:. ecl-trans-halt2(ds;da;v)(n,L)  (n  ecl-trans-es(v)))
(& (n:.
(& ((L':event-info(ds;da) List. L'  L & ecl-halt(ds;da;a)(n,L'))  ecl-trans-halt2(ds;da;v)(n,L))
(& (m:. ecl-act(ds;da;m;a)(L)  ecl-trans-act(ds;da;v)(m,L)))
 (n:.
 ((L':event-info(ds;da) List.
 ((L'  L & 0<n & star-append(event-info(ds;da);ecl-halt(ds;da;a)(0);ecl-halt(ds;da;a)(n))(L'))
 (
 (ecl-trans-halt2(ds;da;reset-ecl-tuple(v))(n,L)) 

latex

Definitions

x:A. B(x), P  Q, {T}, t  T, x. t(x), Prop, AB, A, False, ij, , P & Q, P  Q, x:A. B(x), P  Q, S  T, A & B, ecl-trans-halt2(ds;da;A), T, True, reset-ecl-tuple(A), ecl-trans-h(v), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), if b t else f fi, false, true, ||as||, Y, Top, ecl-trans-tuple{i:l}(ds;da), ecl-trans-type(A), 1of(t), P  Q, x(s), , Unit, l1  l2, Dec(P), b, , ecl-trans-state(v;L)

Lemmas

nat wf, length wf1, non neg length, event-info wf, ecl-trans-tuple wf, ecl wf, fpf wf, Knd wf, Id wf, le wf, nat properties, ge wf, iseg wf, star-append wf, ecl-halt wf, ecl-trans-halt2 wf, reset-ecl-tuple wf, ecl-trans-normal wf, nat plus wf, nat plus inc, l member wf, ecl-trans-es wf, iff wf, ecl-act wf, ecl-trans-act wf, star-append-iff, iseg weakening, iseg transitivity, assert wf, squash wf, true wf, bool wf, ecl-trans-h wf, ecl-trans-state wf, ecl-reset-state, ecl-halt-unique, common iseg compat, ecl-trans-type wf, eq int wf, iff transitivity, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, append wf, length append, add functionality wrt eq, ecl-halt-nil, member wf, iseg append0, append assoc, ecl-trans-state-append, top wf, ecl-trans-state-from wf, ecl-reset-init, decidable functionality, decidable assert, decl-state wf, ma-valtype wf, subtype rel self, length-append, append iseg, bfalse wf